Inference at * 2 1 1 
Iof proof for Lemma before last:

.....rewrite subgoal..... NILNIL

1. T : Type
2. T List
3. u : T
4. v : T List
5. x:T. (x  v)  ((x = last(v)))  x before last(v)  v
6. x : T
7. x = u
8. (x = last([u / v]))
  (null(v)) 

latex

 by ((((((((((((ParallelOp (-1)) 
CollapseTHEN (RW assert_pushdownC (-1)))) 
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)))) 

C(CollapseTHEN (HypSubst (-1) 0))) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))) 

C(CollapseTHEN (Try ((((Unfold `last` 0) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term))))) 

latex

C1: 

C1: 8. v = []
C1: 9. z : T List
C1:   (null([u / z]))
C.

Definitions	, ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), Y, ||as||, l[i], t  T, last(L), A, P  Q, P & Q, P  Q, False, x:A. B(x)
Lemmas	null wf, assert wf, last wf, assert of null